g:Mon, a, b:|g|. Dec(a = b) 

latex

Up	groups 1
Definitions of Statement	Mon
Definitions	t  T, x:A. B(x), P & Q, , P  Q, x f y, P  Q, Mon, IsEqFun(T;eq), P  Q
Lemmas	mon wf, grp car wf, mon properties, decidable assert, grp eq wf, assert wf, decidable functionality